Vérification formelle des processus workflow: Extension aux workflows inter-organisationnels
Identifieur interne : 001684 ( Main/Exploration ); précédent : 001683; suivant : 001685Vérification formelle des processus workflow: Extension aux workflows inter-organisationnels
Auteurs : Zohra Sbaï [Tunisie] ; Kamel Barkaoui [France]Source :
- Ingénierie des systèmes d'information : (2001) [ 1633-1311 ] ; 2013.
Descripteurs français
- Pascal (Inist)
English descriptors
- KwdEn :
Abstract
Workflow technology is currently facing the management of workflow processes that extend across multiple organizations (inter-organizational workflows). To avoid any inconsistencies that may occur during the execution of these workflows, a pre verification is required. Using the model checker SPIN, we present in this paper an approach to formal verification of the soundness properties of these workflows taking into account the resource dimension. To do this, we specify their specification in Promela and the associated soundness properties in LTL.
Affiliations:
Links toward previous steps (curation, corpus...)
- to stream PascalFrancis, to step Corpus: 000031
- to stream PascalFrancis, to step Curation: 000966
- to stream PascalFrancis, to step Checkpoint: 000026
- to stream Main, to step Merge: 001697
- to stream Main, to step Curation: 001684
Le document en format XML
<record><TEI><teiHeader><fileDesc><titleStmt><title xml:lang="fr" level="a">Vérification formelle des processus workflow: Extension aux workflows inter-organisationnels</title><author><name sortKey="Sbai, Zohra" sort="Sbai, Zohra" uniqKey="Sbai Z" first="Zohra" last="Sbaï">Zohra Sbaï</name><affiliation wicri:level="4"><inist:fA14 i1="01"><s1>SysCom, ENIT, Université de Tunis El Manar, BP 37 Le Belvédère</s1><s2>1002, Tunis</s2><s3>TUN</s3><sZ>1 aut.</sZ></inist:fA14><country>Tunisie</country><placeName><settlement type="city">Tunis</settlement><region nuts="2">Gouvernorat de Tunis</region></placeName><orgName type="university">Université de Tunis - El Manar</orgName></affiliation></author><author><name sortKey="Barkaoui, Kamel" sort="Barkaoui, Kamel" uniqKey="Barkaoui K" first="Kamel" last="Barkaoui">Kamel Barkaoui</name><affiliation wicri:level="3"><inist:fA14 i1="02"><s1>CEDRIC, Conservatoire National des Arts et Métiers, Rue Saint Martin</s1><s2>75141, Paris</s2><s3>FRA</s3><sZ>2 aut.</sZ></inist:fA14><country>France</country><placeName><region type="region">Île-de-France</region><region type="old region">Île-de-France</region><settlement type="city">Paris</settlement></placeName></affiliation></author></titleStmt><publicationStmt><idno type="wicri:source">INIST</idno><idno type="inist">14-0038839</idno><date when="2013">2013</date><idno type="stanalyst">PASCAL 14-0038839 INIST</idno><idno type="RBID">Pascal:14-0038839</idno><idno type="wicri:Area/PascalFrancis/Corpus">000031</idno><idno type="wicri:Area/PascalFrancis/Curation">000966</idno><idno type="wicri:Area/PascalFrancis/Checkpoint">000026</idno><idno type="wicri:explorRef" wicri:stream="PascalFrancis" wicri:step="Checkpoint">000026</idno><idno type="wicri:doubleKey">1633-1311:2013:Sbai Z:verification:formelle:des</idno><idno type="wicri:Area/Main/Merge">001697</idno><idno type="wicri:Area/Main/Curation">001684</idno><idno type="wicri:Area/Main/Exploration">001684</idno></publicationStmt><sourceDesc><biblStruct><analytic><title xml:lang="fr" level="a">Vérification formelle des processus workflow: Extension aux workflows inter-organisationnels</title><author><name sortKey="Sbai, Zohra" sort="Sbai, Zohra" uniqKey="Sbai Z" first="Zohra" last="Sbaï">Zohra Sbaï</name><affiliation wicri:level="4"><inist:fA14 i1="01"><s1>SysCom, ENIT, Université de Tunis El Manar, BP 37 Le Belvédère</s1><s2>1002, Tunis</s2><s3>TUN</s3><sZ>1 aut.</sZ></inist:fA14><country>Tunisie</country><placeName><settlement type="city">Tunis</settlement><region nuts="2">Gouvernorat de Tunis</region></placeName><orgName type="university">Université de Tunis - El Manar</orgName></affiliation></author><author><name sortKey="Barkaoui, Kamel" sort="Barkaoui, Kamel" uniqKey="Barkaoui K" first="Kamel" last="Barkaoui">Kamel Barkaoui</name><affiliation wicri:level="3"><inist:fA14 i1="02"><s1>CEDRIC, Conservatoire National des Arts et Métiers, Rue Saint Martin</s1><s2>75141, Paris</s2><s3>FRA</s3><sZ>2 aut.</sZ></inist:fA14><country>France</country><placeName><region type="region">Île-de-France</region><region type="old region">Île-de-France</region><settlement type="city">Paris</settlement></placeName></affiliation></author></analytic><series><title level="j" type="main">Ingénierie des systèmes d'information : (2001)</title><title level="j" type="abbreviated">Ing. syst. inf. : (2001)</title><idno type="ISSN">1633-1311</idno><imprint><date when="2013">2013</date></imprint></series></biblStruct></sourceDesc><seriesStmt><title level="j" type="main">Ingénierie des systèmes d'information : (2001)</title><title level="j" type="abbreviated">Ing. syst. inf. : (2001)</title><idno type="ISSN">1633-1311</idno></seriesStmt></fileDesc><profileDesc><textClass><keywords scheme="KwdEn" xml:lang="en"><term>Business process</term><term>Extension</term><term>Formal method</term><term>Formal verification</term><term>Groupware</term><term>Interoperability</term><term>Linear logic</term><term>Model checking</term><term>Program verification</term><term>Static analysis</term><term>Temporal logic</term><term>Workflow</term></keywords><keywords scheme="Pascal" xml:lang="fr"><term>Workflow</term><term>Vérification programme</term><term>Collecticiel</term><term>Interopérabilité</term><term>Vérification modèle</term><term>Méthode formelle</term><term>Logique linéaire</term><term>Logique temporelle</term><term>Processus métier</term><term>Extension</term><term>Analyse statique</term><term>.</term><term>Vérification formelle</term></keywords></textClass></profileDesc></teiHeader><front><div type="abstract" xml:lang="en">Workflow technology is currently facing the management of workflow processes that extend across multiple organizations (inter-organizational workflows). To avoid any inconsistencies that may occur during the execution of these workflows, a pre verification is required. Using the model checker SPIN, we present in this paper an approach to formal verification of the soundness properties of these workflows taking into account the resource dimension. To do this, we specify their specification in Promela and the associated soundness properties in LTL.</div></front></TEI><affiliations><list><country><li>France</li><li>Tunisie</li></country><region><li>Gouvernorat de Tunis</li><li>Île-de-France</li></region><settlement><li>Paris</li><li>Tunis</li></settlement><orgName><li>Université de Tunis - El Manar</li></orgName></list><tree><country name="Tunisie"><region name="Gouvernorat de Tunis"><name sortKey="Sbai, Zohra" sort="Sbai, Zohra" uniqKey="Sbai Z" first="Zohra" last="Sbaï">Zohra Sbaï</name></region></country><country name="France"><region name="Île-de-France"><name sortKey="Barkaoui, Kamel" sort="Barkaoui, Kamel" uniqKey="Barkaoui K" first="Kamel" last="Barkaoui">Kamel Barkaoui</name></region></country></tree></affiliations></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Main/Exploration
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 001684 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Main/Exploration/biblio.hfd -nk 001684 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= Main
|étape= Exploration
|type= RBID
|clé= Pascal:14-0038839
|texte= Vérification formelle des processus workflow: Extension aux workflows inter-organisationnels
}}
| This area was generated with Dilib version V0.6.33. |  |